\begin{tabbing}
$M$.rframe($A$.effect $f$ of $k$ on $y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$$\in$dom(($M$.2.2.2.2.2.2.2.2.2.2).1). \+
\\[0ex]
\\[0ex]$L$\==($M$.2.2.2.2.2.2.2.2.2.2).1($x$) $\Rightarrow$ \+
\\[0ex]($\uparrow$deq{-}member(KindDeq;$k$;$L$))
\-\\[0ex]$\vee$ ($\forall$$s_{1}$, $s_{2}$:$A$.state, $v$:$A$.da($k$). ($s_{1}$ $\equiv$ $s_{2}$ mod $x$) $\Rightarrow$ ($f$($s_{1}$,$v$) = $f$($s_{2}$,$v$)))
\-
\end{tabbing}